Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.


QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MATCH_25(x, l', a_4, l_3, Pair2(l1, l2)) -> TEST2(a_4, x)
MATCH_42(l_5, Cons2(a, l')) -> PART2(a, l')
APPEND2(l1_2, l2_1) -> MATCH_03(l1_2, l2_1, l1_2)
MATCH_13(a_4, l_3, Cons2(x, l')) -> PART2(a_4, l')
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> APPEND2(quick1(l1), Cons2(a, quick1(l2)))
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l1)
QUICK1(l_5) -> MATCH_42(l_5, l_5)
MATCH_42(l_5, Cons2(a, l')) -> MATCH_54(a, l', l_5, part2(a, l'))
MATCH_03(l1_2, l2_1, Cons2(x, l)) -> APPEND2(l, l2_1)
MATCH_25(x, l', a_4, l_3, Pair2(l1, l2)) -> MATCH_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
MATCH_13(a_4, l_3, Cons2(x, l')) -> MATCH_25(x, l', a_4, l_3, part2(a_4, l'))
PART2(a_4, l_3) -> MATCH_13(a_4, l_3, l_3)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l2)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MATCH_25(x, l', a_4, l_3, Pair2(l1, l2)) -> TEST2(a_4, x)
MATCH_42(l_5, Cons2(a, l')) -> PART2(a, l')
APPEND2(l1_2, l2_1) -> MATCH_03(l1_2, l2_1, l1_2)
MATCH_13(a_4, l_3, Cons2(x, l')) -> PART2(a_4, l')
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> APPEND2(quick1(l1), Cons2(a, quick1(l2)))
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l1)
QUICK1(l_5) -> MATCH_42(l_5, l_5)
MATCH_42(l_5, Cons2(a, l')) -> MATCH_54(a, l', l_5, part2(a, l'))
MATCH_03(l1_2, l2_1, Cons2(x, l)) -> APPEND2(l, l2_1)
MATCH_25(x, l', a_4, l_3, Pair2(l1, l2)) -> MATCH_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
MATCH_13(a_4, l_3, Cons2(x, l')) -> MATCH_25(x, l', a_4, l_3, part2(a_4, l'))
PART2(a_4, l_3) -> MATCH_13(a_4, l_3, l_3)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l2)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 5 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
QDP
            ↳ QDPOrderProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PART2(a_4, l_3) -> MATCH_13(a_4, l_3, l_3)
MATCH_13(a_4, l_3, Cons2(x, l')) -> PART2(a_4, l')

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


MATCH_13(a_4, l_3, Cons2(x, l')) -> PART2(a_4, l')
The remaining pairs can at least be oriented weakly.

PART2(a_4, l_3) -> MATCH_13(a_4, l_3, l_3)
Used ordering: Polynomial interpretation [21]:

POL(Cons2(x1, x2)) = 1 + x2   
POL(MATCH_13(x1, x2, x3)) = 1 + x3   
POL(PART2(x1, x2)) = 1 + x2   

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
QDP
                ↳ DependencyGraphProof
          ↳ QDP
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PART2(a_4, l_3) -> MATCH_13(a_4, l_3, l_3)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 1 less node.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
QDP
            ↳ QDPOrderProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MATCH_03(l1_2, l2_1, Cons2(x, l)) -> APPEND2(l, l2_1)
APPEND2(l1_2, l2_1) -> MATCH_03(l1_2, l2_1, l1_2)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


MATCH_03(l1_2, l2_1, Cons2(x, l)) -> APPEND2(l, l2_1)
The remaining pairs can at least be oriented weakly.

APPEND2(l1_2, l2_1) -> MATCH_03(l1_2, l2_1, l1_2)
Used ordering: Polynomial interpretation [21]:

POL(APPEND2(x1, x2)) = x1   
POL(Cons2(x1, x2)) = 1 + x2   
POL(MATCH_03(x1, x2, x3)) = x3   

The following usable rules [14] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
QDP
                ↳ DependencyGraphProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND2(l1_2, l2_1) -> MATCH_03(l1_2, l2_1, l1_2)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 1 less node.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
QDP
            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MATCH_42(l_5, Cons2(a, l')) -> MATCH_54(a, l', l_5, part2(a, l'))
QUICK1(l_5) -> MATCH_42(l_5, l_5)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l2)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l1)

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be oriented strictly and are deleted.


MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l2)
MATCH_54(a, l', l_5, Pair2(l1, l2)) -> QUICK1(l1)
The remaining pairs can at least be oriented weakly.

MATCH_42(l_5, Cons2(a, l')) -> MATCH_54(a, l', l_5, part2(a, l'))
QUICK1(l_5) -> MATCH_42(l_5, l_5)
Used ordering: Polynomial interpretation [21]:

POL(Cons2(x1, x2)) = 1 + x1 + x2   
POL(False) = 1   
POL(MATCH_42(x1, x2)) = 1 + x2   
POL(MATCH_54(x1, x2, x3, x4)) = 1 + x4   
POL(Nil) = 0   
POL(Pair2(x1, x2)) = 1 + x1 + x2   
POL(QUICK1(x1)) = 1 + x1   
POL(True) = 1   
POL(match_13(x1, x2, x3)) = 1 + x1 + x3   
POL(match_25(x1, x2, x3, x4, x5)) = 1 + x1 + x5   
POL(match_37(x1, x2, x3, x4, x5, x6, x7)) = 1 + x1 + x2 + x3 + x7   
POL(part2(x1, x2)) = 1 + x1 + x2   
POL(test2(x1, x2)) = 1   

The following usable rules [14] were oriented:

match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
test2(x_0, y) -> True
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
test2(x_0, y) -> False
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
QDP
                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

QUICK1(l_5) -> MATCH_42(l_5, l_5)
MATCH_42(l_5, Cons2(a, l')) -> MATCH_54(a, l', l_5, part2(a, l'))

The TRS R consists of the following rules:

test2(x_0, y) -> True
test2(x_0, y) -> False
append2(l1_2, l2_1) -> match_03(l1_2, l2_1, l1_2)
match_03(l1_2, l2_1, Nil) -> l2_1
match_03(l1_2, l2_1, Cons2(x, l)) -> Cons2(x, append2(l, l2_1))
part2(a_4, l_3) -> match_13(a_4, l_3, l_3)
match_13(a_4, l_3, Nil) -> Pair2(Nil, Nil)
match_13(a_4, l_3, Cons2(x, l')) -> match_25(x, l', a_4, l_3, part2(a_4, l'))
match_25(x, l', a_4, l_3, Pair2(l1, l2)) -> match_37(l1, l2, x, l', a_4, l_3, test2(a_4, x))
match_37(l1, l2, x, l', a_4, l_3, False) -> Pair2(Cons2(x, l1), l2)
match_37(l1, l2, x, l', a_4, l_3, True) -> Pair2(l1, Cons2(x, l2))
quick1(l_5) -> match_42(l_5, l_5)
match_42(l_5, Nil) -> Nil
match_42(l_5, Cons2(a, l')) -> match_54(a, l', l_5, part2(a, l'))
match_54(a, l', l_5, Pair2(l1, l2)) -> append2(quick1(l1), Cons2(a, quick1(l2)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 2 less nodes.